mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...

, a Herbrand interpretation is an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the

function Function or functionality may refer to: Computing * Function key, a type of key on computer keyboards * Function model, a structured representation of processes in a system * Function object or functor or functionoid, a concept of object-oriente ...

that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant

Herbrand base In first-order logic, a Herbrand structure ''S'' is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. The idea is to take the symbols of terms as their values, e.g. the denotation of a constant symbol ' ...

, effectively specifying which

ground atom In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables. In first-order logic with identity, the sentence Q(a) \lor P(b) ...

s are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely

syntactic In linguistics, syntax () is the study of how words and morphemes combine to form larger units such as phrases and sentences. Central concerns of syntax include word order, grammatical relations, hierarchical sentence structure (constituency), ...

way, separated from any real instantiation. The importance of Herbrand interpretations is that, if any interpretation satisfies a given set of

clauses In language, a clause is a constituent that comprises a semantic predicand (expressed or not) and a semantic predicate. A typical clause consists of a subject and a syntactic predicate, the latter typically a verb phrase composed of a verb with ...

''S'' then there is a Herbrand interpretation that satisfies them. Moreover,

Herbrand's theorem Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for ...

states that if ''S'' is unsatisfiable then there is a finite unsatisfiable set of ground instances from the

Herbrand universe In first-order logic, a Herbrand structure ''S'' is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. The idea is to take the symbols of terms as their values, e.g. the denotation of a constant symbol '' ...

defined by ''S''. Since this set is finite, its unsatisfiability can be verified in finite time. However, there may be an infinite number of such sets to check. It is named after

Jacques Herbrand Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Cour ...

Notes

Mathematical logic {{mathlogic-stub

See also

Notes